\section{Skolemovské štandardné formuly}

Budeme sa zaoberať procedúram založených na Herbrandovej myšlienke vyvrátenia 
(nájdenie interpretácie, ktorá vyvracia danú formulu).
Davis a Putnam pracovali s formulou v prefixovom
normálnom tvare a vychádzali z nasledujúcich hľadísk:
\begin{enumerate}
%%% {{{
    \item Každá formula logiky 1. rádu
        môže byť vyjadrená v prefixovom normálnom tvare.

    \item Pretože matica (jadro) neobsahuje kvantifikátory, môže byť
        vyjadrená v konjunktívnej normálnej forme.

    \item Zachovajúc nesplniteľnosť formoly z nej môžeme eliminovať
        existenčné kvantifikátory pomocou tzv. skolemovských funkcií (keď máme
        premennú vyjadrenú v prefixovom normálnom tvare a eliminujeme z nej
        existenčný kvantifikátor, dostaneme formulu, ktorá je nesplniteľná
        vtedy, keď je nesplniteľná pôvodná formula -- nesplniteľnosť
        transformovanej formuly sa robí ľahšie).
%%% }}}        
\end{enumerate}

Transformácia formuly:
Majme formulu $A: (Q_1 x_1) (Q_2 x_2) \ldots (Q_n x_n) M$,
kde $M$ je konjunktívnom normálnom tvare.
Nech $Q_r$ je existenčný kvantifikátor v prefixe $(Q_1 x_1) \ldots
(Q_n x_n)$, $1 \le r \le n$.

Uvažujme, že vľavo od $Q_r$ nestojí žiaden veľký kvantifikátor.
Vtedy, ak z prefixu vynechám $(Q_r x_r)$ a $x_r$ v $M$ nahradím
novou konštantou $c_r$ a mám formulu, ktorá je nesplniteľná práve
vtedy, keď bola nesplniteľná pôvodná formula.

Na druhej strane, naľavo od $Q_r$ sa môžu vyskytovať všeobecné
kvantifikátory, $Q_{s_1}, Q_{s_2}, \dots Q_{S_m}$,
kde $1 \le s_1 < s_2 < \dots < s_m < r$.
Vtedy opäť odstránime $(Q_r x_r)$ z prefixu a
za premennú $x_r$ dosadíme do $M$ term 
$f(x_{s_1}, \ldots, x_{s_m})$. Takúto funkciu voláme skolemovaská
funkcia a podobne, takúto konštantu $c$ voláme skolemovská konštanta.

Tento postup môžeme zopakovať pre všetky existenčné kvantifikátory a
výsledok nazveme štandardnou skolemovskou formou.

\begin{priklad}
%%% {{{
    Nájdite štandardnú formu pre formuly:
    \begin{equation*}
        (\exists x) (\forall y) (\forall z) (\exists u) (\forall v) (\exists w)
        P(x,y,z,u,v,w)
    \end{equation*}
    Premennú $x$ budeme nahrádzať konštantou $c$ (ktorá nie je v predikáte),
    premennú $u$ nahradíme $f(y,z)$ a
    premennú $w$ nahradíme funkciou $g(y,z,v)$. Výsledkom je
    \begin{equation*}
        (\forall y)(\forall z)(\forall w) P(c,y,z,f(y,z),v,g(y,z,v))
    \end{equation*}
%%% }}}    
\end{priklad}

\begin{priklad}
%%% {{{
    Nájdite štandardnú formu pre formulu:
    \begin{equation*}
        (\forall x)(\exists y) (\exists z) 
        \left[ (\neg P(x,y) \land Q(x,z))\lor R(x,y,z)\right]
    \end{equation*}
    Využijeme distributívne zákony pre logické spojky a dostaneme
    \begin{equation*}
        (\forall x) (\exists y) (\exists z)
        \left[ \Big(\neg P(x,y) \lor R(x,y,z)\Big) \land
            \Big(Q(x,z)\lor R(x,y,z)\Big)\right]
    \end{equation*}
    a po Skolemizácii máme
    \begin{equation*}
        (\forall x) \left[
            \Big(\neg P(x,f(x)) \lor R(x,f(x),g(x)) \Big) \land
            \Big( Q(x,g(x))\lor R(x,f(x),g(x) \Big) \right]
    \end{equation*}
%%% }}}    
\end{priklad}

\begin{poznamka}
    Formula môže mať viacero štandardných foriem.
\end{poznamka}




\begin{definicia}[Literál]
    Atóm (predikát), alebo jeho negácia.
\end{definicia}

\begin{definicia}[Klauzula]
    Disjunkcia literálov.
    Špeciálne \emph{jednotková klauzula} (tiež jednoliterálna klauzula)
    obsahuje jeden literál. 
\end{definicia}

\begin{definicia}[Prázdna klauzula]
    Klauzala neobsahujúca žiaden literál, (označujeme ju $\varepsilon$).
    Prázdna klauzula je nesplniteľná, pretože neobsahuje žiaden
    literál, ktorý by mohol byť splniteľný.    
\end{definicia}
\begin{poznamka}
    Ak sa nad tým, zamyslíme, definovali sme si nesplniteľnosť
    prázdnej klauzuly tak, aby výraz $\varepsilon \lor K$ bol
    ekvivalentný výrazu $K$ a aby nesplniteľnosť výrazu
    $\varepsilon \land K$ bola ekvivalentná nesplniteľnosti
    výrazu $K$.
\end{poznamka}

\begin{poznamka}
    Štandardná skolemovská forma sa dá zadať aj v množinovom zápise.
    Presnejšie povedané, štandardná forma je konjunkcia klauzulí a
    za jej množinu budeme považovať množinu týchto klauzúl.
    Takýto zápis budeme často využívať a ako uvidíme, tieto dva zápisy
    sú si plne ekvivalentné, čo sa týka nesplniteľnosti.
\end{poznamka}


\begin{priklad}
%%% {{{
    Uvažujme formulu $P \land Q \land \neg R$.\footnote{
    Toman na tomto mieste píše $P \lor Q \lor \neg R$, som si však
    takmer istý, že to pôvodne myslel opačne.
    }
    Ako vieme ju zapísať ako
    množinu klauzúl v konjunkcii nasledovne
    $\{P, Q, \neg R\}$.
    Podobne, pre štandardnú formu
    \begin{equation*}
        (\forall x) \left[
            \Big(\neg P(x,f(x)) \lor R(x,f(x),g(x)) \Big) \land
            \Big( Q(x,g(x))\lor R(x,f(x),g(x) \Big) \right]
    \end{equation*}
    z minulého príkladu vieme spraviť ekvivalentný množinový zápis ako
    \begin{equation*}
        \left\{
            \neg P(x,f(x)) \lor R(x,f(x),g(x)), \quad
            Q(x,g(x))\lor R(x,f(x),g(x) 
        \right\}
    \end{equation*}
%%% }}}    
\end{priklad}

\begin{veta}
    Nech $\mathscr{S}$ je množina klauzúl, ktoré tvoria štandardnú
    formu formuly $A$. Potom $A$ nie je splniteľná $\iff$ $\mathscr{S}$
    nie je splniteľná.
\end{veta}

\begin{dokaz}
%%% {{{
    Uvažujme formulu $A$ tvaru $A: (Q_1 x_1) \dots (Q_n x_n) M[x_1, \dots x_n]$.
    Nech $Q_r$ je prvý existenčný kvantifikátor, čiže $A$ je tvaru
    $(\forall x_1) (\forall x_2) \dots (\forall x_{r-1}) (\exists x_r)
     (Q_{r+1} x_{r+1}) \dots (Q_n x_n) M[x_1, \dots x_n]$.
    Existenčný kvantifikátor nahradíme novou $(r-1)$-árnou funkciou $f$ a
    dostávame formulu $A_1$ v tvare
    \begin{equation*}
        A_1: (\forall x_1) \dots (\forall x_{r-1}) (Q_{r+1} x_{r+1})  \dots (Q_n x_n)
                M[x_1, \dots, x_{r-1}, f(x_1, \dots, x_{r-1}), x_{r+1}, x_n]
    \end{equation*}

    \noindent Tvrdíme, že $A$ nie je splniteľná práve vtedy keď $A_1$ nie je splniteľná:
    \begin{itemize}
    %%% {{{
    \item[$\Rightarrow:$] Sporom. Nech $A_1$ je splniteľná.
        Potom  existuje taká interpretácia $I$, 
        že $I$ vyhovuje $A_1$ ( $A_1$ je pravdivé v $I$).
        To znamená, že pre všetky $x_1 , \dots, x_{r-1}$ existuje také $x_r$,
        ktoré je rovné $f(x_1, \dots, x_{r-1})$.
        Tá istá interpretácia teda vyhovuje aj pôvodnej formule $A$.

    \item[$\Leftarrow:$] Opäť sporom. Nech $A$ je splniteľná.
        Teda existuje interpretácia $I$, ktorá vyhovuje formule $A$.
        Potom pre každú $r-1$-ticu $x_1, \dots, x_{r-1}$ 
        existuje také $x_r$, že platí 
        $M[x_1, \dots, x_{r-1}, x_r, \dots, x_n]$.
        Rozšírme $I$ o $(r-1)$-árny funkčný 
        symbol $f$ tak, že $f(x_1, \dots, x_{r-1}) = x_r$. Potom $I'$
        vyhovyje formule $A_1$ a teda dostávame spor.
    %%% }}}
    \end{itemize}

    \noindent Pokračujme ďalej v dôkaze:
    Označme pôvodnú formulu ako $A_0$. Potom môžeme dosiahnuť štandardnú formu
    $S$ ako postupnosť $A_0, A_1, \dots, A_m$, kde každý krok je zámena prvého
    existenčného kvantifikátora vo formule $A_i$.
    Ak $A_i$ nie je splniteľná, tak ani $A_{i+1}$ nie je splniteľná.
    Tým pádom $A_0$ nie je splniteľná $\iff$ $A_1$ nie je splniteľná $\iff
    \dots \iff$ $A_m\equiv S$ nie je splniteľná.
    No a $S$ nie je splniteľná práve vtedy keď $\mathscr{S}$ nie je
    splniteľná.\footnote{Viď poznámku \ref{poznamka:standard_konj}.}
    \\
%%% }}}
\end{dokaz}

\begin{poznamka}
    Ak $A$ \emph{nie je splniteľná}, tak nesplniteľnosť $A$ je
    ekvivalentná nesplniteľnosti množinovej verzie štandardnej formy
    $\mathscr{S}$, teda môžeme písať
    $A \equiv \mathscr{S}$.
\end{poznamka}

\begin{poznamka}
    Ak $A$ je splniteľná, tak tvrdenie neplatí.
    Majme formulu $A$, ktorá je $A: (\exists x) P(x)$.
    Tým pádom štandardná forma $S$ je $S: P(a)$ 
    ($x$ sme nahradili skolemovskou konštantou $a$).
    Vezmime interpretáciu s univerzom $D = \{1, 2 \}$,
    pričom $a$ priradíme v $I$ hodnotu $1$.
    Hodnoty pre $P$ budú $P(1)=false, P(2)=true$.
    Potom ale $A$ je splniteľná v $I$ (existuje také $x$, menovite
    $2$), lenže $P(a)$ nie je splniteľná v interpretácii $I$.
    Preto $A \not \equiv S$.
\end{poznamka}

\begin{poznamka}
    Z predchádzajúcej poznámky sa ukazuje, že metódy dokazovania
    formúl budú založené na vyvrátení negácie.
\end{poznamka}

\begin{poznamka}
    \label{poznamka:standard_konj}
    Majme formulu $A: A_1 \land A_2 \land \ldots \land A_n$.
    Pre každé $A_i$ si vytvoríme štandardnú formulu $S_i$.
    Potom štandardná forma pre $A$ je 
    $\mathscr{S}=\mathscr{S_1} \union \mathscr{S_2} 
                \union \ldots \union \mathscr{S_m}$,
    kde $\mathscr{S_i}$ je množina klauzúl štandardnej formu $S_i$.
    Formula $A$ nie je splniteľná práve vtedy, keď nie je 
    splniteľná množina klauzúl $\mathscr{S}$.
\end{poznamka}

\begin{priklad}[Z teórie grúp]
    Uvedieme príklad, kde sa pokúsime zapísať pomocou množiny
    klauzúl tvrdenie z teórie grúp. 

    \par Uvažujme grupu a na nej operáciu $\circ$.
    Platia nasledovné axiomy:
    \begin{itemize}
    %%% {{{
        \item [$A_1:$] $x, y \in G \Rightarrow x \circ y \in G$ --
                vlastnosť uzavretosti.
        \item [$A_2:$] $x, y, z \in G \Rightarrow 
                        (x \circ y) \circ z = x \circ (y \circ z)$ --
                asociatívnosť operácie.
        \item [$A_3:$] $x \in G \Rightarrow x \circ e = e \circ x = x$ --
                existencia neutrálneho prvku.
        \item [$A_4:$] $x \in G \Rightarrow \exists x^{-1} \in G :
                            x \circ x^{-1} = e = x^{-1} \circ x$ --
                existencia inverzného prvku.
    %%% }}}
    \end{itemize}

    Chceme ukázať, že ak pre všetky $x \in G$ platí $x \circ x = e$,
    potom je grupa komutatívna. Prvou časťou úlohy je formalizovanie zadania:
    Nech $P(x,y,z)$ označuje\footnote{ % o tom, ze to ma Toman zle
        %%% {{{
        Na tomto mieste by som poznamenal, že to má Toman spravené
        výrazne pofidérne.
        Totiž, nahradením funkcie predikátom sme stratili jednoznačnosť
        funkčnej hodnoty, teda, momentálne môže platiť
        $P(x,y,z) \land P(x,y,z') \land z \ne z'$. Jednoduchou
        interpretáciou, ktorá spĺňa všetky axiómy je napríklad
        $P \equiv true$ a evidentne takáto realizácia nie je teóriou grúp.

        Na druhej strane, spomínaná Tomanova teória je korektná.
        Pointa tkvie v tom, že Tomanova teória {\it nemá}
        predikát rovnosti (čo ruší naše argumenty). Mohlo by sa zdať,
        že daná teória je potom akosi oklieštená, čo aj je.
        Predikát rovnosti ``$a=b$'' sa ale formálne dá nahradiť predikátom
        ``$P(a,e,b)$''. Takto definovaná ``rovnosť'' vyhovuje všetkým
        axiómam rovnosti a navyše sa v nej nedá použiť protipríklad
        uvedený vyššie. Teória je teda v poriadku.
        %%% }}}
    }
    $x \circ y = z$ a nech  $i(x) = x^{-1}$.

    Prepísané axiómy vyzerajú nasledovne:
    \begin{align*}
    %%% {{{
        A_1':\ &(\forall x) (\forall y) (\exists z) P(x,y,z) \\
        A_2': 
            \begin{split}
                & \phantom{\land (} (\forall x) (\forall y) (\forall z)
                (\forall u) (\forall v) (\forall w)
                [ (P(x,y,u) \land  P(y,z,v) \land \highlighta{P(u, z,w)})
                    \implies \highlightc{P(x,v,w)}] \\ 
                &\land (\forall x) (\forall y)(\forall z)
                (\forall u)(\forall v) (\forall w)
                [(P(x,y,u) \land P(y,z,v) \land \highlightc{P(x,v,w)})
                    \implies \highlighta{P(u,z,w)}]
            \end{split} \\
        A_3':\ &(\forall x) P(x,e,x) \land (\forall x) P(e,x,x) \\
        A_4':\ &(\forall x) P(x,i(x),e) \land (\forall x) P(i(x),x,e)
    %%% }}}
    \end{align*}

    Späť k nášmu tvrdeniu. Chceme ukázať
    \begin{align*}
    %%% {{{
        &(\forall x \in G : x \circ x =e) \then
            (\forall u,v \in G: u \circ v = v \circ u) \\
        B':\ & (\forall x) P(x,x,e) \implies  
            (\forall u) (\forall v) [P(u,v,w) \implies P(v,u,w)]
    %%% }}}
    \end{align*}

    Teraz potrebujeme ukázať, že
    $A_1' \land A_2' \land A_3' \land  A_4' \implies B'$.
    Vytvoríme negáciu výroku a ukážeme, že nie je splniteľná:
    \begin{align*}
        F':\ & \neg (A_1' \land A_2' \land A_3' \land A_4') \lor B' \\
      \neg F':\ & A_1' \land A_2' \land A_3' \land A_4' \land \neg B'
    \end{align*}

    Ideme vytvárať množinu klauzúl. Prevedením $A_1', A_2', A_3', A_4'$ do
    štandardnej formy dostávame
    \begin{align*}
    %%% {{{
        \mathscr{S}_1:\ & \Big\{ P(x,y,f(x,y)) \Big\} \\
        \mathscr{S}_2:\ 
            \begin{split}
                 &\Big\{ \neg P(x,y,u) \lor \neg P(y,z,v)
                    \lor \neg P(u,z,w) \lor P(x,v,w), \\
                 &\ \ \neg P(x,y,u)\lor \neg P(y,z,v) \lor \neg P(x,v,q)
                    \lor P(u,z,w) \Big\}
            \end{split} \\
        \mathscr{S}_3:\ & \Big\{ P(x,e,x), \ P(e,x,x) \Big\} \\
        \mathscr{S}_4:\ & \Big\{ P(x,i(x),e), \ P(i(x),x,e) \Big\}
    %%% }}}
    \end{align*}

    Ostáva nám vyjadriť $\neg B'$ ako množinu $\mathscr{B}$.
    \begin{align*}
    %%% {{{
        \neg B':\ &
            \neg [(\forall x) P(x,x,e) \implies
                    (\forall u) (\forall v)(\forall w)(P(u,v,w) \implies
                    P(v,u,w))] \iff \\
        & \neg [ \neg (\forall x) (P(x,x,e)
                \lor (\forall u) (\forall v) (\forall w)
                    (\neg P(u,v,w) \lor P(v,u,w))] \iff \\
        &(\forall x) (P(x,x,e) \land \neg (\forall u)(\forall v) (\forall w) 
          [\neg P(u,v,w) \lor (P(v,u,w)] \iff \\
        & (\forall x) P(x,x,e)
            \land (\exists u) (\exists v) (\exists w)
                    [P(u,v,w)\land \neg P(v,u,w)]
    %%% }}}
    \end{align*}

    Množina $\mathscr{B}$ je potom
    \begin{equation*}
        \mathscr{B}:\  \Big\{P(x,x,e),\ P(a,b,c),\ \neg P(b,a,c) \Big\}
    \end{equation*}

    Máme dokázať, že množina klauzúl 
    $\mathscr{S} = \mathscr{S}_1 \union \mathscr{S}_2 \union
        \mathscr{S}_3 \union \mathscr{S}_4 \union \mathscr{B}$
    nie je splniteľná. Teda pre každú oblasť a interpretáciu je
    nesplniteľná.
    Bolo by teda potrebné vyšetriť všetky oblasti.
    Toto je ale príliš zložité -- overiť niečo na všetkých možných
    oblastiach je nad naše sily.
    Nám ale bude stačiť vyšetrovať na {\it Herbrandovskom univerze},
    ako si ukážeme v nasledujúcej stati.
\end{priklad}
